Nuprl Lemma : nequal_wf
12,41
postcript
pdf
A
:Type,
x
,
y
:
A
.
x
y
A
latex
ProofTree
Definitions
a
b
T
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
origin
A:Type, x, y:A. x 
y 
A 
A:Type, x, y:A. x y A
b T Tx:A. B(x)